package ch.epfl.lara.pm.analyze

import ch.epfl.lara.pm.ast._
import ch.epfl.lara.pm.parser.{NScalaParser,PrettyPrinter}
import ch.epfl.lara.pm.util.MyImplicitConversions
import ch.epfl.lara.pm.formdecider._
import ch.epfl.lara.pm.transformation.MatchAnalyzer
import ch.epfl.lara.pm.util.Tester
import ch.epfl.lara.pm.analyze.set.PatternMap

import scala.util.parsing.combinator._ 
import scala.collection.immutable.HashSet
import ch.epfl.lara.pm.parser.PrettyPrinter
 

object TestVerification extends Tester with InferSetConstraints with MyImplicitConversions{
  import Util._

  def main(args: Array[String]) {
    val program = parseAndTransform(args(0))
    
    
    for(val m: Match <- findMatchExpressions(program)) { 
      constraintsOf(m.tpe,program) match {  
        case None => 
          println("No set-constraint has been found in the program for "+m.tpe+"! Are you sure you is that simple ...")
          verify(m,BTrue)
        case Some(formula) =>
          verify(m,formula)
      }
    }
    
    
  
  }
  
  
  private def verify(m: Match, formula: Formula) = {
    val v = new Verify(formula,List(True),m,new PatternMap)
    v.initialize
    println("-----------------------------")
    PrettyPrinter(m)
    println
    complete(v)
    disjoint(v)
    reachable(v)
    println("-----------------------------\n")
  }
  
  
  private def complete(v: Verify) = {
    v.verifyCompleteness match {
      case None => println("Checking completeness SUCCEDED.\n")
      case Some(warning) => 
        PrettyPrinter(warning)
    }
    println
  }

  private def disjoint(v: Verify) = {
    v.verifyDisjointness match {
      case None => println("Check of disjointness SUCCEDED.\n")
      case Some(warning) =>
        PrettyPrinter(warning)
    }
    println
  }
  
  
  private def reachable(v: Verify) = {
    v.verifyReachability match {
      case None => println("Checking reachability SUCCEDED.\n")
      case Some(unreachable) =>
        PrettyPrinter(unreachable)
    }
    println
  }
  
}
